<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Libraries IPC | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Libraries IPC</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="sel4-libraries-ipc">seL4 Libraries: IPC</h1>

<p>The tutorial is designed to
teach the basics of seL4 IPC using Endpoint objects, and userspace
paging management. You’ll be led through the process of creating a new
thread (retyping an untyped object into a TCB object), and also made to
manually do your own memory management to allocate some virtual memory
for use as the shared memory buffer between your two threads.</p>

<p>Don’t gloss over the globals declared before <code class="language-plaintext highlighter-rouge">main()</code> – they’re declared
for your benefit so you can grasp some of the basic data structures.</p>

<p>You’ll observe that the things you’ve already covered in the second
tutorial are filled out and you don’t have to repeat them: in much the
same way, we won’t be repeating conceptual explanations on this page, if
they were covered by a previous tutorial in the series.</p>

<p>Learning outcomes:</p>

<ul>
  <li>Repeat the spawning of a thread. “'’If it’s nice, do it twice’’”
      – Caribbean folk-saying. Once again, the new thread will be
      sharing its creator’s VSpace and CSpace.</li>
  <li>Introduction to the idea of badges, and minting badged copies of
      an Endpoint capability. NB: you don’t mint a new copy of the
      Endpoint object, but a copy of the capability that
      references it.</li>
  <li>Basic IPC: sending and receiving: how to make two
      threads communicate.</li>
  <li>IPC Message format, and Message Registers. seL4 binds some of
      the first Message Registers to hardware registers, and the rest
      are transferred in the IPC buffer.</li>
  <li>Understand that each thread has only one IPC buffer, which is
      pointed to by its TCB. It’s possible to make a thread wait on
      both an Endpoint and a Notification using “Bound Notifications”.</li>
  <li>Understand CSpace pointers, which are really just integers with
      multiple indexes concatenated into one. Understanding them well
      however, is important to understanding how capabilities work.</li>
</ul>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/libraries-1">Libraries: initialisation &amp; threading</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> libraries-2
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-2_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> libraries-2
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-2_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="exercises">Exercises</h2>

<p>When you first run this tutorial, you will see a fault as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
Caught cap fault in send phase at address (nil)
while trying to handle:
vm fault on data at address 0x70003c8 with status 0x6
in thread 0xffffff801ffb5400 "rootserver" at address 0x402977
With stack:
0x43df70: 0x0
0x43df78: 0x0
</code></pre></div></div>

<h3 id="allocate-an-ipc-buffer">Allocate an IPC buffer</h3>

<p>As we mentioned in passing before, threads in seL4 do their own memory
management. You implement your own Virtual Memory Manager, essentially.
To the extent that you must allocate a physical memory frame, then map
it into your thread’s page directory – and even manually allocate page
tables on your own, where necessary.</p>

<p>Here’s the first step in a conventional memory manager’s process of
allocating memory: first allocate a physical frame. As you would expect,
you cannot directly write to or read from this frame object since it is
not mapped into any virtual address space as yet. Standard restrictions
of a MMU-utilizing kernel apply.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 1: get a frame cap for the ipc buffer */
    /* hint: vka_alloc_frame()
     * int vka_alloc_frame(vka_t *vka, uint32_t size_bits, vka_object_t *result)
     * @param vka Pointer to vka interface.
     * @param size_bits Frame size: 2^size_bits
     * @param result Structure for the Frame object.  This gets initialised.
     * @return 0 on success
     */
    vka_object_t ipc_frame_object;
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">vka_alloc_frame</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="n">IPCBUF_FRAME_SIZE_BITS</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ipc_frame_object</span><span class="p">);</span>
    <span class="n">ZF_LOGF_IFERR</span><span class="p">(</span><span class="n">error</span><span class="p">,</span> <span class="s">"Failed to alloc a frame for the IPC buffer.</span><span class="se">\n</span><span class="s">"</span>
                  <span class="s">"</span><span class="se">\t</span><span class="s">The frame size is not the number of bytes, but an exponent.</span><span class="se">\n</span><span class="s">"</span>
                  <span class="s">"</span><span class="se">\t</span><span class="s">NB: This frame is not an immediately usable, virtually mapped page.</span><span class="se">\n</span><span class="s">"</span><span class="p">)</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output will not change.</p>

<h3 id="try-to-map-a-page">Try to map a page</h3>

<p>Take note of the line of code that precedes this: the one where a
virtual address is randomly chosen for use. This is because, as we
explained before, the process is responsible for its own Virtual Memory
Management. As such, if it chooses, it can map any page in its VSpace to
physical frame. It can technically choose to do unconventional things,
like not unmap PFN #0. The control of how the address space is managed
is up to the threads that have write-capabilities to that address space.
There is both flexibility and responsibility implied here. Granted, seL4
itself provides strong guarantees of isolation even if a thread decides
to go rogue.</p>

<p>Attempt to map the frame you allocated earlier, into your VSpace. A keen
reader will pick up on the fact that it’s unlikely that this will work,
since you’d need a new page table to contain the new page-table-entry.
The tutorial deliberately walks you through both the mapping of a frame
into a VSpace, and the mapping of a new page-table into a VSpace.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/arch_include/x86/vspace/arch/page.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/arch_include/x86/vspace/arch/page.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/interfaces/sel4arch.xml">https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/interfaces/sel4arch.xml</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 2: try to map the frame the first time  */
    /* hint 1: seL4_ARCH_Page_Map()
     * The *ARCH* versions of seL4 sys calls are abstractions over the architecture provided by libsel4utils
     * this one is defined as:
     * #define seL4_ARCH_Page_Map seL4_X86_Page_Map
     * The signature for the underlying function is:
     * int seL4_X86_Page_Map(seL4_X86_Page service, seL4_X86_PageDirectory pd, seL4_Word vaddr, seL4_CapRights rights, seL4_X86_VMAttributes attr)
     * @param service Capability to the page to map.
     * @param pd Capability to the VSpace which will contain the mapping.
     * @param vaddr Virtual address to map the page into.
     * @param rights Rights for the mapping.
     * @param attr VM Attributes for the mapping.
     * @return 0 on success.
     *
     * Note: this function is generated during build.  It is generated from the following definition:
     *
     * hint 2: for the rights, use seL4_AllRights
     * hint 3: for VM attributes use seL4_ARCH_Default_VMAttributes
     * Hint 4: It is normal for this function call to fail. That means there are
     *    no page tables with free slots -- proceed to the next step where you'll
     *    be led to allocate a new empty page table and map it into the VSpace,
     *    before trying again.
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_ARCH_Page_Map</span><span class="p">(</span><span class="n">ipc_frame_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">pd_cap</span><span class="p">,</span> <span class="n">ipc_buffer_vaddr</span><span class="p">,</span>
                               <span class="n">seL4_AllRights</span><span class="p">,</span> <span class="n">seL4_ARCH_Default_VMAttributes</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output will be as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>libraries-2: main@main.c:260 [Err seL4_FailedLookup]:
	Failed to allocate new page table.
</code></pre></div></div>

<h3 id="allocate-a-page-table">Allocate a page table</h3>

<p>So just as you previously had to manually retype a new frame to use for
your IPC buffer, you’re also going to have to manually retype a new
page-table object to use as a leaf page-table in your VSpace.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
        /* TASK 3: create a page table */
        /* hint: vka_alloc_page_table()
         * int vka_alloc_page_table(vka_t *vka, vka_object_t *result)
         * @param vka Pointer to vka interface.
         * @param result Structure for the PageTable object.  This gets initialised.
         * @return 0 on success
         */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="n">vka_object_t</span> <span class="n">pt_object</span><span class="p">;</span>
        <span class="n">error</span> <span class="o">=</span>  <span class="n">vka_alloc_page_table</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">pt_object</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, you will see another fault.</p>

<h3 id="map-a-page-table">Map a page table</h3>

<p>If you successfully retyped a new page table from an untyped memory
object, you can now map that new page table into your VSpace, and then
try again to finally map the IPC-buffer’s frame object into the VSpace.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/arch_include/x86/vspace/arch/page.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/arch_include/x86/vspace/arch/page.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/interfaces/sel4arch.xml">https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/interfaces/sel4arch.xml</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
        /* TASK 4: map the page table */
        /* hint 1: seL4_ARCH_PageTable_Map()
         * The *ARCH* versions of seL4 sys calls are abstractions over the architecture provided by libsel4utils
         * this one is defined as:
         * #define seL4_ARCH_PageTable_Map seL4_X86_PageTable_Map
         * The signature for the underlying function is:
         * int seL4_X86_PageTable_Map(seL4_X86_PageTable service, seL4_X86_PageDirectory pd, seL4_Word vaddr, seL4_X86_VMAttributes attr)
         * @param service Capability to the page table to map.
         * @param pd Capability to the VSpace which will contain the mapping.
         * @param vaddr Virtual address to map the page table into.
         * @param rights Rights for the mapping.
         * @param attr VM Attributes for the mapping.
         * @return 0 on success.
         *
         * Note: this function is generated during build.  It is generated from the following definition:
         *
         * hint 2: for VM attributes use seL4_ARCH_Default_VMAttributes
         */
</code></pre></div></div>

<p>On completion, you will see another fault.</p>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_ARCH_PageTable_Map</span><span class="p">(</span><span class="n">pt_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">pd_cap</span><span class="p">,</span>
                                        <span class="n">ipc_buffer_vaddr</span><span class="p">,</span> <span class="n">seL4_ARCH_Default_VMAttributes</span><span class="p">);</span>
</code></pre></div>  </div>

</details>

<h3 id="map-a-page">Map a page</h3>

<p>Use <code class="language-plaintext highlighter-rouge">seL4_ARCH_Page_Map</code> to map the frame in.
If everything was done correctly, there is no reason why this step
should fail. Complete it and proceed.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
        /* TASK 5: then map the frame in */
        /* hint 1: use seL4_ARCH_Page_Map() as above
         * hint 2: for the rights, use seL4_AllRights
         * hint 3: for VM attributes use seL4_ARCH_Default_VMAttributes
         */

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>        <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_ARCH_Page_Map</span><span class="p">(</span><span class="n">ipc_frame_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">pd_cap</span><span class="p">,</span>
                                   <span class="n">ipc_buffer_vaddr</span><span class="p">,</span> <span class="n">seL4_AllRights</span><span class="p">,</span> <span class="n">seL4_ARCH_Default_VMAttributes</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, you will see the following:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>main: hello world
libraries-2: main@main.c:464 [Cond failed: seL4_MessageInfo_get_length(tag) != 1]
	Response data from thread_2 was not the length expected.
	How many registers did you set with seL4_SetMR within thread_2?
</code></pre></div></div>

<h3 id="allocate-an-endpoint">Allocate an endpoint</h3>

<p>Now we have a (fully mapped) IPC buffer – but no Endpoint object to
send our IPC data across. We must retype an untyped object into a kernel
Endpoint object, and then proceed. This could be done via a more
low-level approach using <code class="language-plaintext highlighter-rouge">seL4_Untyped_Retype()</code>, but instead, the
tutorial makes use of the VKA allocator. Remember that the VKA allocator
is an seL4 type-aware object allocator? So we can simply ask it for a
new object of a particular type, and it will do the low-level retyping
for us, and return a capability to a new object as requested.</p>

<p>In this case, we want a new Endpoint so we can do IPC. Complete the step
and proceed.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 6: create an endpoint */
    /* hint: vka_alloc_endpoint()
     * int vka_alloc_endpoint(vka_t *vka, vka_object_t *result)
     * @param vka Pointer to vka interface.
     * @param result Structure for the Endpoint object.  This gets initialised.
     * @return 0 on success
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">vka_alloc_endpoint</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ep_object</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output will not change.</p>

<h3 id="badge-an-endpoint">Badge an endpoint</h3>

<p>Badges are used to uniquely identify a message queued on an endpoint as
having come from a particular sender. Recall that in seL4, each thread
has only one IPC buffer. If multiple other threads are sending data to a
listening thread, how can that listening thread distinguish between the
data sent by each of its IPC partners? Each sender must “badge” its
capability to its target’s endpoint.</p>

<p>Note the distinction: the badge is not applied to the target endpoint,
but to the sender’s <strong>capability</strong> to the target endpoint. This
enables the listening thread to mint off copies of a capability to an
Endpoint to multiple senders. Each sender is responsible for applying a
unique badge value to the capability that the listener gave it so that
the listener can identify it.</p>

<p>In this step, you are badging the endpoint that you will use when
sending data to the thread you will be creating later on. The
<code class="language-plaintext highlighter-rouge">vka_mint_object()</code> call will return a new, badged copy of the
capability to the endpoint that your new thread will listen on. When you
send data to your new thread, it will receive the badge value with the
data, and know which sender you are. Complete the step and proceed.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object_capops.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object_capops.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 7: make a badged copy of it in our cspace. This copy will be used to send
     * an IPC message to the original cap */
    /* hint 1: vka_mint_object()
     * int vka_mint_object(vka_t *vka, vka_object_t *object, cspacepath_t *result, seL4_CapRights rights, seL4_Word badge)
     * @param[in] vka The allocator for the cspace.
     * @param[in] object Target object for cap minting.
     * @param[out] result Allocated cspacepath.
     * @param[in] rights The rights for the minted cap.
     * @param[in] badge The badge for the minted cap.
     * @return 0 on success
     *
     * hint 2: for the rights, use seL4_AllRights
     * hint 3: for the badge use EP_BADGE
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">vka_mint_object</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ep_object</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">ep_cap_path</span><span class="p">,</span> <span class="n">seL4_AllRights</span><span class="p">,</span>
                            <span class="n">EP_BADGE</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output will not change.</p>

<h3 id="message-registers">Message registers</h3>

<p>Here we get a formal introduction to message registers. At first glance,
you might wonder why the <code class="language-plaintext highlighter-rouge">sel4_SetMR()</code> calls don’t specify a message
buffer, and seem to know which buffer to fill out – and that would be
correct, because they do. They are operating directly on the sending
thread’s IPC buffer. Recall that each thread has only one IPC buffer. Go
back and look at your call to <code class="language-plaintext highlighter-rouge">seL4_TCB_Configure()</code> in step 7 again:
you set the IPC buffer for the new thread in the last 2 arguments to
this function. Likewise, the thread that created <strong>your</strong> main thread
also set an IPC buffer up for you.</p>

<p>So <code class="language-plaintext highlighter-rouge">seL4_SetMR()</code> and <code class="language-plaintext highlighter-rouge">seL4_GetMR()</code> simply write to and read from the IPC
buffer you designated for your thread. <code class="language-plaintext highlighter-rouge">MSG_DATA</code> is uninteresting – can
be any value. You’ll find the <code class="language-plaintext highlighter-rouge">seL4_MessageInfo_t</code> type explained in the
manuals. In short, it’s a header that is embedded in each message that
specifies, among other things, the number of Message Registers that hold
meaningful data, and the number of capabilities that are going to be
transmitted in the message.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 8: set the data to send. We send it in the first message register */
    /* hint 1: seL4_MessageInfo_new()
     * seL4_MessageInfo_t CONST seL4_MessageInfo_new(seL4_Uint32 label, seL4_Uint32 capsUnwrapped, seL4_Uint32 extraCaps, seL4_Uint32 length)
     * @param label The value of the label field
     * @param capsUnwrapped The value of the capsUnwrapped field
     * @param extraCaps The value of the extraCaps field
     * @param length The number of message registers to send
     * @return The seL4_MessageInfo_t containing the given values.
     *
     * seL4_MessageInfo_new() is generated during build. It can be found in:
     * build/x86/pc99/libsel4/include/sel4/types_gen.h
     *
     * hint 2: use 0 for the first 3 fields.
     * hint 3: send only 1 message register of data
     *
     * hint 4: seL4_SetMR()
     * void seL4_SetMR(int i, seL4_Word mr)
     * @param i The message register to write
     * @param mr The value of the message register
     *
     * hint 5: send MSG_DATA
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">tag</span> <span class="o">=</span> <span class="n">seL4_MessageInfo_new</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">1</span><span class="p">);</span>
    <span class="n">seL4_SetMR</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="n">MSG_DATA</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should change as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>libraries-2: main@main.c:472 [Cond failed: msg != ~MSG_DATA]
	Response data from thread_2's content was not what was expected.
</code></pre></div></div>

<h3 id="ipc">IPC</h3>

<p>Now that you’ve constructed your message and badged the endpoint that
you’ll use to send it, it’s time to send it. The <code class="language-plaintext highlighter-rouge">seL4_Call()</code> syscall
will send a message across an endpoint synchronously. If there is no
thread waiting at the other end of the target endpoint, the sender will
block until there is a waiter. The reason for this is because the seL4
kernel would prefer not to buffer IPC data in the kernel address space,
so it just sleeps the sender until a receiver is ready, and then
directly copies the data. It simplifies the IPC logic. There are also
polling send operations, as well as polling receive operations in case
you don’t want to be forced to block if there is no receiver on the
other end of an IPC Endpoint.</p>

<p>When you send your badged data using <code class="language-plaintext highlighter-rouge">seL4_Call()</code>, our receiving thread
(which we created earlier) will pick up the data, see the badge, and
know that it was us who sent the data. Notice how the sending thread
uses the <strong>badged</strong> capability to the endpoint object, and the
receiving thread uses the unmodified original capability to the same
endpoint? The sender must identify itself.</p>

<p>Notice also that the fact that both the sender and the receiver share
the same root CSpace, enables the receiving thread to just casually use
the original, unbadged capability without any extra work needed to make
it accessible.</p>

<p>Notice however also, that while the sending thread has a capability that
grants it full rights to send data across the endpoint since it was the
one that created that capability, the receiver’s capability may not
necessarily grant it sending powers (write capability) to the endpoint.
It’s entirely possible that the receiver may not be able to send a
response message, if the sender doesn’t want it to.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h">https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 9: send and wait for a reply. */
    /* hint: seL4_Call()
     * seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
     * @param dest The capability to be invoked.
     * @param msgInfo The messageinfo structure for the IPC.  This specifies information about the message to send (such as the number of message registers to send).
     * @return A seL4_MessageInfo_t structure.  This is information about the repy message.
     *
     * hint 2: seL4_MessageInfo_t is generated during build.
     * The type definition and generated field access functions are defined in a generated file:
     * build/x86/pc99/libsel4/include/sel4/types_gen.h
     * It is generated from the following definition:
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">tag</span> <span class="o">=</span> <span class="n">seL4_Call</span><span class="p">(</span><span class="n">ep_cap_path</span><span class="p">.</span><span class="n">capPtr</span><span class="p">,</span> <span class="n">tag</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, you should see thread_2 fault as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>thread_2: hallo wereld
thread_2: got a message 0 from 0
Caught cap fault in send phase at address (nil)
while trying to handle:
vm fault on data at address (nil) with status 0x4
in thread 0xffffff801ffb4400 "child of: 'rootserver'" at address (nil)
in thread 0xffffff801ffb4400 "child of: 'rootserver'" at address (nil)
With stack:
</code></pre></div></div>

<h3 id="receive-a-reply">Receive a reply</h3>

<p>While this task is out of order, since we haven’t yet examined the
receive-side of the operation here, it’s fairly simple anyway: this task
occurs after the receiver has sent a reply, and it shows the sender now
reading the reply from the receiver. As mentioned before, the
<code class="language-plaintext highlighter-rouge">seL4_GetMR()</code> calls are simply reading from the calling thread’s
designated, single IPC buffer.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 10: get the reply message */
    /* hint: seL4_GetMR()
     * seL4_Word seL4_GetMR(int i)
     * @param i The message register to retreive
     * @return The message register value
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">msg</span> <span class="o">=</span> <span class="n">seL4_GetMR</span><span class="p">(</span><span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should not change.</p>

<h3 id="receive-an-ipc">Receive an IPC</h3>

<p>We’re now in the receiving thread. The <code class="language-plaintext highlighter-rouge">seL4_Recv()</code> syscall performs a
blocking listen on an Endpoint or Notification capability. When new data
is queued (or when the Notification is signalled), the <code class="language-plaintext highlighter-rouge">seL4_Recv</code>
operation will unqueue the data and resume execution.</p>

<p>Notice how the <code class="language-plaintext highlighter-rouge">seL4_Recv()</code> operation explicitly makes allowance for
reading the badge value on the incoming message? The receiver is
explicitly interested in distinguishing the sender.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h">https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/syscalls.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 11: wait for a message to come in over the endpoint */
    /* hint 1: seL4_Recv()
     * seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word* sender)
     * @param src The capability to be invoked.
     * @param sender The badge of the endpoint capability that was invoked by the sender is written to this address.
     * @return A seL4_MessageInfo_t structure
     *
     * hint 2: seL4_MessageInfo_t is generated during build.
     * The type definition and generated field access functions are defined in a generated file:
     * build/x86/pc99/libsel4/include/sel4/types_gen.h
     */
</code></pre></div></div>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">tag</span> <span class="o">=</span> <span class="n">seL4_Recv</span><span class="p">(</span><span class="n">ep_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">sender_badge</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should change slightly:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>thread_2: got a message 0 from 0x61
</code></pre></div></div>

<h3 id="validate-the-message">Validate the message</h3>

<p>These two calls here are just verification of the fidelity of the
transmitted message. It’s very unlikely you’ll encounter an error here.
Complete them and proceed to the next step.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 12: make sure it is what we expected */
    /* hint 1: check the badge. is it EP_BADGE?
     * hint 2: we are expecting only 1 message register
     * hint 3: seL4_MessageInfo_get_length()
     * seL4_Uint32 CONST seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo)
     * @param seL4_MessageInfo the seL4_MessageInfo_t to extract a field from
     * @return the number of message registers delivered
     * seL4_MessageInfo_get_length() is generated during build. It can be found in:
     * build/x86/pc99/libsel4/include/sel4/types_gen.h
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">sender_badge</span> <span class="o">!=</span> <span class="n">EP_BADGE</span><span class="p">,</span>
               <span class="s">"Badge on the endpoint was not what was expected.</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>

    <span class="n">ZF_LOGF_IF</span><span class="p">(</span><span class="n">seL4_MessageInfo_get_length</span><span class="p">(</span><span class="n">tag</span><span class="p">)</span> <span class="o">!=</span> <span class="mi">1</span><span class="p">,</span>
               <span class="s">"Length of the data send from root thread was not what was expected.</span><span class="se">\n</span><span class="s">"</span>
               <span class="s">"</span><span class="se">\t</span><span class="s">How many registers did you set with seL4_SetMR, within the root thread?</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should not change.</p>

<h3 id="read-the-message-registers">Read the message registers</h3>

<p>Again, just reading the data from the Message Registers.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 13: get the message stored in the first message register */
    /* hint: seL4_GetMR()
     * seL4_Word seL4_GetMR(int i)
     * @param i The message register to retreive
     * @return The message register value
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">msg</span> <span class="o">=</span> <span class="n">seL4_GetMR</span><span class="p">(</span><span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should change slightly:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>thread_2: got a message 0x6161 from 0x61
</code></pre></div></div>

<h3 id="write-the-message-registers">Write the message registers</h3>

<p>And writing Message Registers again.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 14: copy the modified message back into the message register */
    /* hint: seL4_SetMR()
     * void seL4_SetMR(int i, seL4_Word mr)
     * @param i The message register to write
     * @param mr The value of the message register
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_SetMR</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span> <span class="n">msg</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should not change.</p>

<h3 id="reply-to-a-message">Reply to a message</h3>

<p>This is a formal introduction to the <code class="language-plaintext highlighter-rouge">Reply</code> capability which is
automatically generated by the seL4 kernel, whenever an IPC message is
sent using the <code class="language-plaintext highlighter-rouge">seL4_Call()</code> syscall. This is unique to the <code class="language-plaintext highlighter-rouge">seL4_Call()</code>
syscall, and if you send data instead with the <code class="language-plaintext highlighter-rouge">seL4_Send()</code> syscall, the
seL4 kernel will not generate a Reply capability.</p>

<p>The Reply capability solves the issue of a receiver getting a message
from a sender, but not having a sufficiently permissive capability to
respond to that sender. The “Reply” capability is a one-time capability
to respond to a particular sender. If a sender doesn’t want to grant the
target the ability to send to it repeatedly, but would like to allow the
receiver to respond to a specific message once, it can use <code class="language-plaintext highlighter-rouge">seL4_Call()</code>,
and the seL4 kernel will facilitate this one-time permissive response.
Complete the step and pat yourself on the back.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h">https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h</a></li>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf">https://github.com/seL4/seL4/blob/master/libsel4/mode_include/32/sel4/shared_types.bf</a></li>
</ul>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    /* TASK 15: send the message back */
    /* hint 1: seL4_ReplyRecv()
     * seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
     * @param dest The capability to be invoked.
     * @param msgInfo The messageinfo structure for the IPC.  This specifies information about the message to send (such as the number of message registers to send) as the Reply part.
     * @param sender The badge of the endpoint capability that was invoked by the sender is written to this address.  This is a result of the Wait part.
     * @return A seL4_MessageInfo_t structure.  This is a result of the Wait part.
     *
     * hint 2: seL4_MessageInfo_t is generated during build.
     * The type definition and generated field access functions are defined in a generated file:
     * build/x86/pc99/libsel4/include/sel4/types_gen.h
     * It is generated from the following definition:
     */
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">seL4_ReplyRecv</span><span class="p">(</span><span class="n">ep_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">tag</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">sender_badge</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On completion, the output should change, with the fault message replaced with the following:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>main: got a reply: [0xffff9e9e|0xffffffffffff9e9e]
</code></pre></div></div>

<p>That’s it for this tutorial.</p>



<p style="text-align: right;">

      Next: <a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/libraries-2/libraries-2.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/libraries-2/libraries-2.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#allocate-an-ipc-buffer">Allocate an IPC buffer</a></li>
<li class="toc-entry toc-h3"><a href="#try-to-map-a-page">Try to map a page</a></li>
<li class="toc-entry toc-h3"><a href="#allocate-a-page-table">Allocate a page table</a></li>
<li class="toc-entry toc-h3"><a href="#map-a-page-table">Map a page table</a></li>
<li class="toc-entry toc-h3"><a href="#map-a-page">Map a page</a></li>
<li class="toc-entry toc-h3"><a href="#allocate-an-endpoint">Allocate an endpoint</a></li>
<li class="toc-entry toc-h3"><a href="#badge-an-endpoint">Badge an endpoint</a></li>
<li class="toc-entry toc-h3"><a href="#message-registers">Message registers</a></li>
<li class="toc-entry toc-h3"><a href="#ipc">IPC</a></li>
<li class="toc-entry toc-h3"><a href="#receive-a-reply">Receive a reply</a></li>
<li class="toc-entry toc-h3"><a href="#receive-an-ipc">Receive an IPC</a></li>
<li class="toc-entry toc-h3"><a href="#validate-the-message">Validate the message</a></li>
<li class="toc-entry toc-h3"><a href="#read-the-message-registers">Read the message registers</a></li>
<li class="toc-entry toc-h3"><a href="#write-the-message-registers">Write the message registers</a></li>
<li class="toc-entry toc-h3"><a href="#reply-to-a-message">Reply to a message</a></li>
</ul>
</li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/libraries-2.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/libraries-2.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
